($\lambda$$A$,$T$,$L$,$k$,$i$,$f$,$z$. reduce2($f$;$k$;$i$;$L$))
\\[0ex]$\in$ $A$,$T$:Type$\rightarrow$$L$:($T$ List)$\rightarrow$$A$$\rightarrow$($i$:$\mathbb{N}\rightarrow$($T$$\rightarrow$\{$i$..($i$+$\parallel$$L$$\parallel$)$^{-}$\}$\rightarrow$$A$$\rightarrow$$A$)$\rightarrow\downarrow$True$\rightarrow$$A$)